the_es:ES, T:Type, f:(IdT), g:(IdLnkIdT), e:E.
case(kind(e))act(a) => f(a)rcv(l,tg) => g(l,tg)  T 

latex

Definitions	x:A. B(x), t  T, case(kind(e))act(a) => f(a)rcv(l,tg) => g(l;tg), x(s), x(s1,s2), if b then t else f fi , P  Q, tt, ff, , , Unit, P  Q, P & Q,
Lemmas	es-isrcv wf, bool wf, eqtt to assert, es-lnk wf, es-tag wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-act wf, es-E wf, IdLnk wf, Id wf, event system wf